; benchmark generated from python API
(set-info :status unknown)
(declare-fun spring_edit_thin_feasible () Bool)
(declare-fun spring_edit_thin_kid_0_feasible () Bool)
(declare-fun spring_edit_thin_kid_0_hight () Real)
(declare-fun spring_edit_thin_kid_0_y () Real)
(declare-fun spring_edit_thin_hight () Real)
(declare-fun spring_edit_thin_width () Real)
(declare-fun spring_edit_thin_kid_0_width () Real)
(declare-fun spring_edit_thin_kid_0_x () Real)
(assert
 (let (($x954 (not spring_edit_thin_feasible)))
 (let (($x2098 (or $x954 spring_edit_thin_kid_0_feasible)))
 (let (($x2096 (not spring_edit_thin_kid_0_feasible)))
 (let (($x2097 (or $x2096 spring_edit_thin_feasible)))
 (let ((?x2093 (+ (+ (- spring_edit_thin_hight) spring_edit_thin_kid_0_y) spring_edit_thin_kid_0_hight)))
 (let (($x2095 (or $x954 (= ?x2093 0.0))))
 (let (($x2090 (or $x954 (= spring_edit_thin_kid_0_y 0.0))))
 (let ((?x2086 (- (+ spring_edit_thin_kid_0_x spring_edit_thin_kid_0_width) spring_edit_thin_width)))
 (let (($x2088 (or $x954 (= ?x2086 0.0))))
 (let (($x2084 (or $x954 (= spring_edit_thin_kid_0_x 0.0))))
 (let ((?x2080 (- (- spring_edit_thin_hight spring_edit_thin_kid_0_y) spring_edit_thin_kid_0_hight)))
 (let (($x2082 (or $x954 (>= ?x2080 0.0))))
 (let (($x2069 (>= spring_edit_thin_kid_0_y 0.0)))
 (let (($x2078 (or $x954 $x2069)))
 (let ((?x2075 (+ (- (- spring_edit_thin_kid_0_x) spring_edit_thin_kid_0_width) spring_edit_thin_width)))
 (let (($x2077 (or $x954 (>= ?x2075 0.0))))
 (let (($x2068 (>= spring_edit_thin_kid_0_x 0.0)))
 (let (($x2072 (or $x954 $x2068)))
 (let (($x2071 (>= spring_edit_thin_kid_0_hight 0.0)))
 (let (($x2070 (>= spring_edit_thin_kid_0_width 0.0)))
 (and $x2068 $x2069 $x2070 $x2071 $x2072 $x2077 $x2078 $x2082 $x2084 $x2088 $x2090 $x2095 $x2097 $x2098 spring_edit_thin_feasible))))))))))))))))))))))
(check-sat)

